Nuprl Lemma : filter_trivial2
11,40
postcript
pdf
T
:Type,
P
:(
T
),
L
:(
T
List). (
x
L
.
P
(
x
))
(filter(
P
;
L
) =
L
)
latex
Definitions
x
.
t
(
x
)
,
,
t
T
,
x
(
s
)
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
bool
wf
,
l
member
wf
,
assert
wf
,
l
all
wf
,
filter
trivial
origin
T:Type, P:(T
), L:(T List). (x
L. 
P(x)) 
(filter(P;L) = L) T:Type, P:(T), L:(T List). (xL. P(x)) (filter(P;L) = L) 
x. t(x)
T Qx:A. B(x)